


`include "package.sv"
program assertions(DDR_bus IF);
 
/*  
property tester;
      @(posedge IF.CK)
      $fell(IF.RAS) ##1 $fell(IF.CAS);
endproperty
  
TEST: assert property (tester)
          else $info("RAS to CAS delay error");
 */                    
            
property RASL2RASH;  //verify RAS fall and rise time....should this change?
	$fell(IF.RAS) |-> ##tRCD $rose(IF.RAS);
endproperty

assert property (@(posedge IF.CK) RASL2RASH)
    else $info("RAS delay incorrect");


property CASL2CASH;  //verify CAS fall and rise time
	$fell(IF.CAS) |-> ##tCL $rose(IF.CAS);
endproperty

assert property(@(posedge IF.CK) CASL2CASH)
  else $info("CAS delay incorrect");
    
/*
property ACT2PRE; //verify tRAS time between ACT and following PRE
	@(posedge IF.CK)
	(IF.memory_controller.State == IF.ACTIVATE) ##tRAS (IF.memory_controller.State == IF.PRECHARGE);
endproperty

assert property(@(posedge IF.CK) ACT2PRE)
  else $info ("ACTIVATE to PRECHARGE incorrect delay");


//make sure that RAS falls once row is on line
property ADDR2RAS;  
	@(posedge IF.CK)
	$changed(IF.ADDRESS_LINE)|-> $fell(IF.RAS);
endproperty
*/


property RAS2CAS;  //Verify that CAS falls tRCD after RAS.
	$fell(IF.RAS) |-> ##tRCD $fell(IF.CAS);
endproperty

assert property (@(posedge IF.CK) RAS2CAS)
  else $info("RAS to CAS delay incorrect");


property BURST;
	$changed(IF.DQ) |-> ##tBURST $isunknown(IF.DQ);
endproperty

assert property (@(posedge IF.CK) BURST)
  else $info("Burst length incorrect");

//verify no other activity to a bank until tRP after a PRE

//need RAS2READ. send WE signal HIGH. then after tOE valid data is sent. all within tRC





/*
property RAS2WRITEDATA;
	@(posedge IF.CK)
	$fell(IF.RAS) ##tRAS ($changed(ADDRESS_LINE && $fell(IF.CAS) &&		$fell(IF.WE) && $changed(IF.DQ)));
endproperty



property WRITE2DATA; //WL = AL + CWL
	@(posedge IF.CK)
	(IF.ENUM == WR && $changed(IF.ADDRESS_LINE)) ##(tAL + tCWL) $changed(DQ);
endproperty


property TESTACT;  //test activate property..
//After a row is opened with an ACTIVATE command, a READ or WRITE command may be issued to that row, subject to the tRCD specification. 
//other tests should pick up where this leaves off
	@(posedge IF.CK)
	(IF.ENUM == ACT) |-> ($changed(IF.ADDRESS_LINE) ##[0:tRCD] ((IF.ENUM == RD || IF.ENUM == WR)));
endproperty


property TESTPRE;  //verify precharge time before activate is asserted
	@(posedge IF.CK)
	(IF.ENUM == PRE) ##tRP (IF.ENUM == ACT);
endproperty            
 
 
 
property ADDR2CAS;  //after row and ras, need column and CAS. can overlap
	@(posedge IF.CK)
	(ADDR2RAS |-> ($changed(IF.ADDRESS_LINE) ##tRCD $fell(IF.CAS));
endproperty


property READ2DATA;
	@(posedge IF.CK)
	RAS2CAS ##(tCL+tAL) ($changed(data && IF.DQ && IF.OE));
endproperty

 
 */
  
  
  
endprogram
  
